A:Type, B:(AType).
(a,b:A. decidable((a = b)))
 (a:A, u,v:B(a). decidable((u = v)))
 (x,y:(a:A  B(a)). decidable((x = y))) 

latex

Definitions	P  Q, x(s), prop{i:l}, x:A. B(x), t  T, decidable(P), P  Q, A, guard(T), False, t.2, t.1, x. t(x)
Lemmas	pi1 wf, pi2 wf, not wf, decidable wf